ds:(IdType), da:(IdKndType), A:Type, X:Interface(ds;da;A), es:ES.
es-decl(es;ds;da)  ([[X]]  AbsInterface(A)) 

latex

Definitions

AbsInterface(A), [[X]], in-interface(es;X;e), inr x , if b then t else f fi , interface-val(es;X;e), x.A(x), P  Q, s = t, A, False, E, t.1, es-decl(es;ds;da), Interface(ds;da;A), a:A fp B(a), let x,y = A in B(x;y), t  T, Top, P & Q, constant_function(f;A;B), b, , x:A. B(x), P  Q, r  s, e < e', val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), , , type List, Msg(M), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, EState(T), f(a), EOrderAxioms(E; pred?; info), Id, x:A  B(x), IdLnk, x:AB(x), left + right, Unit, EqDecider(T), Type, ES, ff

Lemmas

bfalse wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, interface-val wf, ifthenelse wf, in-interface wf